the_es:ES, e', e:E. Dec((e <loc e')) 

latex

Definitions	t  T, x:A. B(x), P  Q, Dec(P), ES, (e <loc e'), Prop, E, P  Q, {T}, x. t(x), WellFnd{i}(A;x,y.R(x;y)), first(e), b, False, A, pred(e), P & Q, P  Q, P  Q
Lemmas	es-pred-locl, decidable functionality, es-locl-iff, not wf, assert wf, decidable and, es-pred wf, decidable not, decidable or, decidable es-E equal, es-first-implies, es-locl-wellfnd, es-E wf, decidable wf, es-locl wf, event system wf, decidable assert, es-first wf